\begin{tabbing}
es{-}kind{-}sends{-}iff(${\it es}$;$k$;$A$;$l$;${\it tg}$;$B$;${\it ds}$;$e$.$f$($e$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:es{-}E(${\it es}$). es{-}kind(${\it es}$; $e$) $=$ rcv($l$,${\it tg}$) $\in$ Knd $\Rightarrow$ es{-}valtype(${\it es}$; $e$) $\subseteq\rho$ $B$)\+
\\[0ex]\& ($\forall$$x$:Id. es{-}vartype(${\it es}$; source($l$); $x$) $\subseteq\rho$ fpf{-}cap(${\it ds}$;IdDeq;$x$;Top))
\\[0ex]\& (\=$\forall$$e$:es{-}E(${\it es}$).\+
\\[0ex]es{-}kind(${\it es}$; $e$) $=$ $k$ $\in$ Knd
\\[0ex]$\Rightarrow$ es{-}loc(${\it es}$; $e$) $=$ source($l$) $\in$ Id
\\[0ex]$\Rightarrow$ es{-}valtype(${\it es}$; $e$) $\subseteq\rho$ $A$)
\-\\[0ex]\& \=alle{-}at(${\it es}$;source($l$);$e$.\=es{-}kind(${\it es}$; $e$) $=$ $k$ $\in$ Knd\+\+
\\[0ex]$\Rightarrow$ isl($f$($e$))
\\[0ex]$\Rightarrow$ (\=$\exists$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex]es{-}kind(${\it es}$; ${\it e'}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd
\\[0ex]\& es{-}sender(${\it es}$; ${\it e'}$) $=$ $e$ $\in$ es{-}E(${\it es}$)))
\-\-\\[0ex]\& (\=$\forall$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex]es{-}kind(${\it es}$; ${\it e'}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd
\\[0ex]$\Rightarrow$ \=es{-}kind(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$)) $=$ $k$ $\in$ Knd\+
\\[0ex]\& isl($f$(es{-}sender(${\it es}$; ${\it e'}$)))
\\[0ex]\& es{-}val(${\it es}$; ${\it e'}$) $=$ outl($f$(es{-}sender(${\it es}$; ${\it e'}$))) $\in$ $B$)
\-\-\\[0ex]\& (\=$\forall$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex]es{-}kind(${\it es}$; ${\it e'}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd
\\[0ex]$\Rightarrow$ (\=$\forall$${\it e''}$:es{-}E(${\it es}$).\+
\\[0ex]es{-}kind(${\it es}$; ${\it e''}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd
\\[0ex]$\Rightarrow$ es{-}sender(${\it es}$; ${\it e''}$) $=$ es{-}sender(${\it es}$; ${\it e'}$) $\in$ es{-}E(${\it es}$)
\\[0ex]$\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$ $\in$ es{-}E(${\it es}$)))
\-\-\-\-
\end{tabbing}